Nuprl Lemma : list_accum_wf
11,40
postcript
pdf
T
,
T'
:Type,
l
:(
T
List),
y
:
T'
,
f
:(
T'
T
T'
). list_accum(
x
,
a
.
f
(
x
,
a
);
y
;
l
)
T'
latex
Definitions
x
,
y
.
t
(
x
;
y
)
,
Y
,
x
(
s1
,
s2
)
,
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
member
wf
origin
T,T':Type, l:(T List), y:T', f:(T'
TT'). list_accum(x,a.f(x,a); y; l) 
T' T,T':Type, l:(T List), y:T', f:(T'TT'). list_accum(x,a.f(x,a); y; l) T' 
x,y. t(x;y) Tx:A. B(x)